/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package alloytoy;

import java.io.*;
import java.util.*;
import java.util.logging.Level;
import java.util.logging.Logger;

/**
 * AlloyDif is responsible for computing the diferences between two alloy models.
 *
 *
 * @author Daniel
 */
public class AlloyDif {
    String fileName1;
    String fileName2;
    String fileOutput;
    Map<String, String> sigs;
    Map<String, String> preds;
    Map<String, String> sigs2;
    Map<String, String> preds2;
    ArrayList<String> utilList;
    ArrayList<String> utilList2;
    ArrayList<String> runns1;
    ArrayList<String> runns2;
    Map<String, String> asserts1;
    Map<String, String> asserts2;

    Map<String, String> facts1;
    Map<String, String> facts2;

    public AlloyDif(String f1, String f2, String fout){
        fileName1 = f1;
        fileName2 = f2;
        fileOutput = fout;
        
        sigs = new HashMap<String,String>();
        preds = new HashMap<String,String>();

        sigs2 = new HashMap<String,String>();
        preds2 = new HashMap<String,String>();

        utilList = new ArrayList<String>();
        utilList2 = new ArrayList<String>();

        runns1 = new ArrayList<String>();
        runns2 = new ArrayList<String>();

        asserts1 = new HashMap<String, String>();
        asserts2 = new HashMap<String, String>();

        facts1 = new HashMap<String, String>();
        facts2 = new HashMap<String, String>();
    }

    public void ComputeDiff(AlloyFunctions model){
        
        try {
            BufferedReader bout = new BufferedReader(new FileReader(fileName1));
            String line = null;
            while ((line = bout.readLine()) != null){
                //System.out.println(line);
                if(line.indexOf("assert ")!=-1){
                    NewAssert(line,bout,asserts1);
                }
                if(line.indexOf("run ")!=-1|| line.indexOf("check ")!=-1){
                    runns1.add(line);
                }
                if(line.indexOf("open util")!=-1)
                {
                    //New UtilProcessing
                    //System.out.println(line);
                    utilList.add(line);
                }
                if(line.indexOf("fact ")!=-1){
                    NewAssert(line,bout,facts1);
                }
                if(line.indexOf("sig")!=-1){
                    //New Sig Processing
                    //System.out.println("SIG: "+line);
                    NewSig(line,bout,sigs);
                }
                if(line.indexOf("pred")!=-1){
                    //New pred Processing
                    NewPred(line,bout,preds);
                }
            }

            BufferedReader bout2 = new BufferedReader(new FileReader(fileName2));
            String line2 = null;
            while ((line2 = bout2.readLine()) != null){
                if(line2.indexOf("assert ")!=-1){
                    NewAssert(line2,bout2,asserts1);
                }

                if(line2.indexOf("fact ")!=-1){
                    //System.out.println(line);
                    NewAssert(line2,bout2,facts2);
                }

                if(line2.indexOf("run ")!=-1 || line2.indexOf("check ")!=-1){
                    runns2.add(line2);
                }

                if(line2.indexOf("open util")!=-1)
                {
                    //New UtilProcessing
                    utilList2.add(line2);
                }
                
                if(line2.indexOf("sig")!=-1){
                    //New Sig Processing
                    NewSig(line2,bout2,sigs2);
                }
                if(line2.indexOf("pred")!=-1){
                    //New pred Processing
                    NewPred(line2,bout2,preds2);
                }
            }
            /*System.out.println("NEW DIF");
            System.out.println("SIGS1 BEFORE: "+sigs);
            System.out.println("SIGS2 BEFORE: "+sigs2);
            System.out.println("MODEL BEFORE: "+model.diffSigs);*/
            DiffMaps(sigs,sigs2,model,true);
            //System.out.println("MODEL AFTER: "+model.diffSigs);

            //System.out.println("PREDS BEFORE: "+preds);
            DiffMaps(preds,preds2,model,false);

            DiffMaps(asserts1,asserts2,model,false);
            //System.out.println("FACTS1 : "+facts1);
            //System.out.println("FACTS2 : "+facts2);
            DiffMaps(facts1,facts2,model,false);
            //System.out.println("PREDS AFTER: "+preds);
            //System.out.println("New");
            //System.out.println(DotParser.sortByValue(Main.differences));
            //System.out.println("");

            DiffUtils(utilList,utilList2);
            //System.out.println("RUNNS 1 : " +runns1);
            //System.out.println("RUNNS 2 : "+runns2);
            DiffUtils(runns1,runns2);
            //System.out.println(utilList);

            PrintMapsToFile(utilList,sigs,facts1,preds,runns1,asserts1,fileOutput);
            //System.out.println();
            //System.out.println();

        } catch (FileNotFoundException ex) {
            Logger.getLogger(Main.class.getName()).log(Level.SEVERE, null, ex);
        } catch(IOException ex){
            Logger.getLogger(Main.class.getName()).log(Level.SEVERE, null, ex);
        }
    }

    //For all s in s2 => s in s1
    private static void DiffUtils(ArrayList<String> s1, ArrayList<String> s2){
        for(String s : s2){
            if(!s1.contains(s)) s1.add(s);
        }
    }
    
    private static int countOBracs(String str){
        int count =0;

        for(int i=0; i<str.length(); i++){
            if(str.charAt(i)=='{')
                count++;
        }
        return count;
    }
    private static int countCBracs(String str){
        int count =0;

        for(int i=0; i<str.length(); i++){
            if(str.charAt(i)=='}')
                count++;
        }
        return count;
    }

    //returns only the signature name
    private static String getSigName(String line){
        StringTokenizer st = new StringTokenizer(line);
        st.nextToken();
        String nameBrac = st.nextToken();
        if(nameBrac.indexOf("{")!=-1)
            return nameBrac.substring(0,nameBrac.indexOf("{"));
        return nameBrac;
    }

    //Returns only the predicate name
    private static String getPredName(String line){
        StringTokenizer st = new StringTokenizer(line);
        st.nextToken();
        String nameBrac = st.nextToken();
        if(nameBrac.indexOf("[")!=-1)
            return nameBrac.substring(0,nameBrac.indexOf("["));
        return nameBrac;
    }

    //Inserts the pair (sigName,sigBody) in the map
    private static void NewSig(String line, BufferedReader bout, Map<String,String> sigs) throws IOException{
        String sigName = getSigName(line);
        //System.out.println("NAME: "+sigName);
        //System.out.println("SIG: "+line);
        String body=line.substring(line.indexOf(sigName)+sigName.length());
        body+="\n";
        int cBracs = countCBracs(body);
        int oBracs = countOBracs(body);
        int dif=cBracs-oBracs;
        String tmpLine="";
        while(dif!=0){
            tmpLine = bout.readLine();
            cBracs += countCBracs(tmpLine);
            oBracs += countOBracs(tmpLine);
            dif=cBracs-oBracs;
            //System.out.println("LINE: " + tmpLine);
            body+=tmpLine+"\n";
        }
        //System.out.println("NAME: "+sigName);
        //System.out.println("BODY: "+ body);
        sigs.put(sigName, body);
    }

    //inserts the pair (predName,predBody) in the map
    private static void NewPred(String line, BufferedReader bout, Map<String,String> preds) throws IOException{
        String predName = getPredName(line);
        //System.out.println("NAME: "+predName);

        String body=line.substring(line.indexOf(predName)+predName.length());
        body+="\n";
        int cBracs = countCBracs(body);
        int oBracs = countOBracs(body);
        int dif=cBracs-oBracs;
        String tmpLine="";
        while(dif!=0){
            tmpLine = bout.readLine();
            cBracs += countCBracs(tmpLine);
            oBracs += countOBracs(tmpLine);
            dif=cBracs-oBracs;
            //System.out.println("LINE: " + tmpLine);
            body+=tmpLine+"\n";
        }
        //System.out.println("NAME: "+predName);
        //System.out.println("BODY: "+ body);
        preds.put(predName, body);

    }

    //For all entrys E in map2: map1.put(E.key,E.body)
    private static void DiffMaps(Map<String,String> map1, Map<String,String> map2, AlloyFunctions model, boolean Sigs){
        Iterator it = map2.entrySet().iterator();
        
        if(Sigs){
            model.diffSigs.addAll(map1.keySet());
        }
        while (it.hasNext()) {
            Map.Entry pairs = (Map.Entry)it.next();
            String Key = (String) pairs.getKey();
            map1.put(Key,(String) pairs.getValue());
            if(Main.differences.containsKey(Key)){
                if(Sigs) model.diffSigs.remove(Key);
                 Integer value = (Integer) Main.differences.get(Key);
                 Main.differences.put(Key, value+1);
            }
            else{
                if(Sigs) model.diffSigs.remove(Key);
                Main.differences.put(Key,0);
            }
        }
        
    }

    private static void PrintMapsToFile(ArrayList<String> utilList, Map<String,String> sigs, Map<String,String> facts, Map<String,String> preds,ArrayList<String> runns,Map<String,String> asserts, String fileName) throws FileNotFoundException, IOException{
        BufferedWriter bwrite = new BufferedWriter(new FileWriter(fileName));
        for(String s : utilList){
            bwrite.write(s);
            bwrite.newLine();
        }
        
        Iterator it = sigs.entrySet().iterator();
        while (it.hasNext()) {
            Map.Entry pairs = (Map.Entry)it.next();
            bwrite.write("sig "+(String) pairs.getKey());
            bwrite.write((String) pairs.getValue());
            bwrite.newLine();
            //bwrite.newLine();
        }

        Iterator itf = facts.entrySet().iterator();
        while (itf.hasNext()) {
            Map.Entry pairs = (Map.Entry)itf.next();
            bwrite.write("fact "+(String) pairs.getKey());
            bwrite.write((String) pairs.getValue());
            bwrite.newLine();
            //bwrite.newLine();
        }

        Iterator it2 = preds.entrySet().iterator();
        while (it2.hasNext()) {
            Map.Entry pairs = (Map.Entry)it2.next();
            bwrite.write("pred "+(String) pairs.getKey());
            bwrite.write((String) pairs.getValue());
            bwrite.newLine();
            //bwrite.newLine();
        }

        for(String s : runns){
            if(s!=null){
                bwrite.write(s);
                bwrite.newLine();
                bwrite.newLine();
            }
        }
        //System.out.println(runns);

        Iterator it3 = asserts.entrySet().iterator();
        while (it3.hasNext()) {
            Map.Entry pairs = (Map.Entry)it3.next();
            bwrite.write("assert "+(String) pairs.getKey());
            bwrite.write((String) pairs.getValue());
            bwrite.newLine();
            //bwrite.newLine();
        }
        bwrite.flush();
        bwrite.close();
    }

    //returns only the signature name
    private static String getAssertName(String line){
        StringTokenizer st = new StringTokenizer(line);
        st.nextToken();
        String nameBrac = st.nextToken();
        if(nameBrac.indexOf("{")!=-1)
            return nameBrac.substring(0,nameBrac.indexOf("{"));
        return nameBrac;
    }

    private void NewAssert(String line, BufferedReader bout, Map<String, String> assertsMap) throws IOException {
        String assertName = getAssertName(line);
        //System.out.println(assertName);
        String body=line.substring(line.indexOf(assertName)+assertName.length());
        body+="\n";
        int cBracs = countCBracs(body);
        int oBracs = countOBracs(body);
        int dif=cBracs-oBracs;
        String tmpLine="";
        while(dif!=0){
            tmpLine = bout.readLine();
            cBracs += countCBracs(tmpLine);
            oBracs += countOBracs(tmpLine);
            dif=cBracs-oBracs;
            //System.out.println("LINE: " + tmpLine);
            body+=tmpLine+"\n";
        }
        //System.out.println("NAME: "+assertName);
        //System.out.println("BODY: "+ body);
        assertsMap.put(assertName, body);
    }
}
